(set-logic BV)
(synth-fun f ( (x (BitVec 64)) ) (BitVec 64)
((Start (BitVec 64)
((bvnot Start)
(bvxor Start Start)
(bvand Start Start)
(bvor Start Start)
(bvneg Start)
(bvadd Start Start)
(bvmul Start Start)
(bvudiv Start Start)
(bvurem Start Start)
(bvlshr Start Start)
(bvashr Start Start)
(bvshl Start Start)
(bvsdiv Start Start)
(bvsrem Start Start)
(bvsub Start Start)
x
#x0000000000000000
#x0000000000000001
#x0000000000000002
#x0000000000000003
#x0000000000000004
#x0000000000000005
#x0000000000000006
#x0000000000000007
#x0000000000000008
#x0000000000000009
#x0000000000000009
#x0000000000000009
#x000000000000000A
#x000000000000000B
#x000000000000000C
#x000000000000000D
#x000000000000000E
#x000000000000000F
#x0000000000000010
(ite StartBool Start Start)
))
(StartBool Bool
((= Start Start)
(not StartBool)
(and StartBool StartBool)
(or StartBool StartBool)
))))
(constraint (= (f #x2c5496e25e3b2c1e) #xe9d5b48ed0e269f0))
(constraint (= (f #xd84e4e9143dae3c2) #x93d8d8b75e128e1e))
(constraint (= (f #xb020a153215e6ae0) #xe0c3c7eec7fdffc0))
(constraint (= (f #xa7d7e9897aece615) #xac140b3b42898cf5))
(constraint (= (f #x8a6b218781b20b67) #x3dfec71f07ec3fde))
(constraint (= (f #x625e63ade56b2852) #xced0ce290d4a6bd6))
(constraint (= (f #xed539a5bd972b740) #x895632d21346a45f))
(constraint (= (f #x1aa3c049ce9eea19) #xf2ae1fdb18b08af3))
(constraint (= (f #xe831b33b1691287d) #xf0e7eefe7f66f1fe))
(constraint (= (f #x922a47a4cb1c6409) #xb6eadc2d9a71cdfb))
(constraint (= (f #x53bcd9820ebde9de) #xd621933ef8a10b10))
(constraint (= (f #x281c3ddeb2b23d9d) #xebf1e110a6a6e131))
(constraint (= (f #xd702e8a7aee683ad) #xfe0ff3dfffdf0ffe))
(constraint (= (f #x7cce37281e351c6e) #xfbbcfef07cfe79fc))
(constraint (= (f #x36487317043862a8) #xfdb1ee7e18f1cff0))
(constraint (= (f #x8a1b3cddddc9ab34) #x3c7efbffffb7fef8))
(constraint (= (f #xc0b05da2c1670488) #x9fa7d12e9f4c7dbb))
(constraint (= (f #xcdd3027987e085ee) #xbfee0df71fc31ffc))
(constraint (= (f #x525db5a055548269) #xedffffc1fffb0df6))
(constraint (= (f #xe0dbe42615846ac4) #x8f920decf53dca9d))
(constraint (= (f #xeb3a5d7e1538c5d4) #x8a62d140f5639d15))
(constraint (= (f #xd757819ae1cae999) #x94543f328f1a8b33))
(constraint (= (f #x3089d6e87e36e81d) #xe7bb148bc0e48bf1))
(constraint (= (f #x555d9641e8b83c71) #xffff7d87f3f0f9e6))
(constraint (= (f #x61c0ad7d6e9ebe04) #xcf1fa94148b0a0fd))
(constraint (= (f #xd1e6d4e4237be43c) #xe7dffbd8cfffd8f8))
(constraint (= (f #x53ebb22ede6920e7) #xefffecfffdf6c3de))
(constraint (= (f #x5eddde211cd5c430) #xfffffcc67bff98e0))
(constraint (= (f #x439ce14b2a389798) #xde318f5a6ae3b433))
(constraint (= (f #xb070d548ebe92e2d) #xe1e3ffb3fff6fcfe))
(constraint (= (f #xec44eae7d02e2a80) #x89dd8a8c17e8eabf))
(constraint (= (f #xbe8423100b8913ec) #xff18ce603f366ff8))
(constraint (= (f #x2ab8d5eceea0e7cc) #xeaa3950988af8c19))
(constraint (= (f #x4b8e66bea65c576c) #xbf3ddfffddf9fff8))
(constraint (= (f #x3eca7b514eb990e8) #xffbdffe7bff763f0))
(constraint (= (f #xe9c18d805d8a6b86) #x8b1f393fd13aca3c))
(constraint (= (f #x330cb2e735e4d66c) #xee3befdeffdbfdf8))
(constraint (= (f #x797b9d4e2aaedbae) #xf7ff7fbcfffffffc))
(constraint (= (f #xb1ad2d4cb40ea2cb) #xa7296959a5f8ae9a))
(constraint (= (f #xb37e4854b40d45ca) #xa640dbd5a5f95d1a))
(constraint (= (f #x0ee12b246dbca3e5) #x3fc6fed9fffbcfde))
(constraint (= (f #xebca82e0eaa9459b) #x8a1abe8f8aab5d32))
(constraint (= (f #xe62d1519e7be0ede) #x8ce975730c20f890))
(constraint (= (f #xe3817b887298459e) #x8e3f423bc6b3dd30))
(constraint (= (f #x9a1c8d72b955bce9) #x7c7b3feff7fffbf6))
(constraint (= (f #xc1d0c4a3059e88b6) #x87e39bce1f7f33fc))
(constraint (= (f #xcb30d5e2dbc63c6d) #xbee3ffcfff9cf9fe))
(constraint (= (f #x2447d50cc47c730c) #xeddc15799dc1c679))
(constraint (= (f #x813d18ec9c91d151) #xbf617389b1b71757))
(constraint (= (f #x348ce4e292de9765) #xfb3bdbcf6fff7fde))
(constraint (= (f #xbced407d0ec7e977) #xfbff81fe3f9ff7fe))
(constraint (= (f #x0bae9308a89c10dd) #xfa28b67babb1f791))
(constraint (= (f #xbebda888b37cee1e) #xa0a12bbba64188f0))
(constraint (= (f #x42843e93edac5e7a) #x8f18ff6ffff9fdfc))
(constraint (= (f #x4194d8c74e2cce16) #xdf35939c58e998f4))
(constraint (= (f #xeb25d433beb4a512) #x8a6d15e620a5ad76))
(constraint (= (f #x84551987ad302364) #x19fe771ffee0cfd8))
(constraint (= (f #xa45c730bdcc706b0) #xd9f9ee3ffb9e1fe0))
(constraint (= (f #xeee4471cba9ebe5e) #x888ddc71a2b0a0d0))
(constraint (= (f #x8a69ce82e9e29cd0) #xbacb18be8b0eb197))
(constraint (= (f #x9e108d2aed1cc17a) #x7c633efffe7b87fc))
(constraint (= (f #x913d324d2e4d7b48) #xb76166d968d9425b))
(constraint (= (f #xec980e6b3104ee1c) #x89b3f8ca677d88f1))
(constraint (= (f #x0e68e89ae8eb3e64) #x3df3f37ff3fefdd8))
(constraint (= (f #xd943aae40e99382d) #xf78fffd83f76f0fe))
(constraint (= (f #x80e0d7e920c66eee) #x03c3fff6c39dfffc))
(constraint (= (f #x2bae6e07e5eea684) #xea28c8fc0d08acbd))
(constraint (= (f #xaeede5541c2a82b3) #xffffdff878ff0fee))
(constraint (= (f #xca2c46634dba2b85) #x9ae9dcce5922ea3d))
(constraint (= (f #xe4e610747630bdd5) #x8d8cf7c5c4e7a115))
(constraint (= (f #xc6422e7a83e235c7) #x9cdee8c2be0ee51c))
(constraint (= (f #x84ae19c47e4b5da2) #x1bfc7799fdbfffcc))
(constraint (= (f #x142b41d8b489ee3e) #x78ff87f3fb37fcfc))
(constraint (= (f #x2ec9c07ea14709ae) #xffb781ffc79e37fc))
(constraint (= (f #xb68251610e8e1403) #xa4bed74f78b8f5fe))
(constraint (= (f #x2cb2d8a8e4b33ea9) #xfbeff3f3dbeefff6))
(constraint (= (f #x1e4987dd39dd0ebe) #x7db71ffef7fe3ffc))
(constraint (= (f #x75d9ba11293e6b5a) #xc51322f76b60ca52))
(constraint (= (f #x812ec89eeb48ab81) #xbf689bb08a5baa3f))
(constraint (= (f #xe34604902eedb343) #x8e5cfdb7e889265e))
(constraint (= (f #xaeea2b55bdb85a99) #xa88aea552123d2b3))
(constraint (= (f #x16b813e6cec4815a) #xf4a3f60c989dbf52))
(constraint (= (f #x7b2eed769c2002d8) #xc2688944b1effe93))
(constraint (= (f #x8a7e8575d2164276) #x3dff1fffec7d8dfc))
(constraint (= (f #x781661d35b93b9dc) #xc3f4cf1652362311))
(constraint (= (f #xdc4deaa701b39927) #xf9bfffde07ef76de))
(constraint (= (f #x6896cc459a8d8783) #xcbb499dd32b93c3e))
(constraint (= (f #xc56790633a525891) #x9d4c37ce62d6d3b7))
(constraint (= (f #x3b76774bca13d3aa) #xfffdffbfbc6feffc))
(constraint (= (f #xd8d1b868d035096e) #xf3e7f1f3e0fe37fc))
(constraint (= (f #xd7e7a0a7e39e7ea7) #xffdfc3dfcf7dffde))
(constraint (= (f #x59b35556baa1e543) #xd3265554a2af0d5e))
(constraint (= (f #x26a1c5e9175ec737) #xdfc79ff67fff9efe))
(constraint (= (f #xe677dea0d2a9c482) #x8cc410af96ab1dbe))
(constraint (= (f #x85a1e772971d443e) #x1fc7dfef7e7f98fc))
(constraint (= (f #xd835ecd40e8b3611) #x93e50995f8ba64f7))
(constraint (= (f #x7169253e610e06be) #xe7f6defdc63c1ffc))
(constraint (= (f #xaa2cee1240103b14) #xaae988f6dff7e275))
(constraint (= (f #x0aac07762407e927) #x3ff81ffcd81ff6de))
(constraint (= (f #xce76e40d66167b31) #xbdffd83fdc7dfee6))
(check-synth)
